T:Type, a, b:T List. l_disjoint(T;b;a)  l_disjoint(T;a;b) 

latex

Definitions	P & Q, False, P  Q, A, t  T, x:A. B(x), (x  l), Prop, l_disjoint(T;l1;l2), P  Q, P  Q
Lemmas	l disjoint wf, l member wf